Theory Timestamp
theory Timestamp
imports "HOL-Library.Extended_Nat" "HOL-Library.Extended_Real"
begin
class timestamp = comm_monoid_add + semilattice_sup +
fixes tfin :: "'a set" and ι :: "nat â 'a"
assumes ι_mono: "âi j. i ⤠j ⹠ι i ⤠ι j"
and ι_fin: "âi. ι i â tfin"
and ι_progressing: "x â tfin â¹ âj. ¬ι j ⤠ι i + x"
and zero_tfin: "0 â tfin"
and tfin_closed: "c â tfin â¹ d â tfin â¹ c + d â tfin"
and add_mono: "c ⤠d ⹠a + c ⤠a + d"
and add_pos: "a â tfin â¹ 0 < c â¹ a < a + c"
begin
lemma add_mono_comm:
fixes a :: 'a
shows "c ⤠d ⹠c + a ⤠d + a"
by (auto simp: add.commute add_mono)
end
instantiation prod :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
begin
definition zero_prod :: "'a à 'b" where
"zero_prod = (zero_class.zero, zero_class.zero)"
fun plus_prod :: "'a à 'b â 'a à 'b â 'a à 'b" where
"(a, b) + (c, d) = (a + c, b + d)"
instance
by standard (auto simp: zero_prod_def ac_simps)
end
instantiation enat :: timestamp
begin
definition tfin_enat :: "enat set" where
"tfin_enat = UNIV - {â}"
definition ι_enat :: "nat â enat" where
"ι_enat n = n"
instance
by standard (auto simp add: ι_enat_def tfin_enat_def dest!: leD)
end
instantiation ereal :: timestamp
begin
definition ι_ereal :: "nat â ereal" where
"ι_ereal n = ereal n"
definition tfin_ereal :: "ereal set" where
"tfin_ereal = UNIV - {-â, â}"
lemma ereal_add_pos:
fixes a :: ereal
shows "a â tfin â¹ 0 < c â¹ a < a + c"
by (auto simp: tfin_ereal_def) (metis add.right_neutral ereal_add_cancel_left ereal_le_add_self order_less_le)
instance
by standard (auto simp add: ι_ereal_def tfin_ereal_def add.commute
ereal_add_le_add_iff2 not_le less_PInf_Ex_of_nat ereal_less_ereal_Ex reals_Archimedean2 intro: ereal_add_pos)
end
class timestamp_strict = timestamp +
assumes timestamp_strict_total: "a ⤠b ⨠b ⤠a"
and add_mono_strict: "c < d â¹ a + c < a + d"
instantiation nat :: timestamp_strict
begin
definition tfin_nat :: "nat set" where
"tfin_nat = UNIV"
definition ι_nat :: "nat â nat" where
"ι_nat n = n"
instance
by standard (auto simp add: ι_nat_def tfin_nat_def dest!: leD)
end
instantiation real :: timestamp_strict
begin
definition tfin_real :: "real set" where "tfin_real = UNIV"
definition ι_real :: "nat â real" where "ι_real n = real n"
instance
by standard (auto simp: tfin_real_def ι_real_def not_le reals_Archimedean2)
end
class timestamp_total = timestamp +
assumes timestamp_total: "a ⤠b ⨠b ⤠a"
assumes aux: "0 ⤠a â¹ a ⤠c â¹ a â tfin â¹ c â tfin â¹ 0 ⤠b â¹ b â tfin â¹ c < a + b"
instantiation enat :: timestamp_total
begin
instance
apply standard
apply (auto simp: tfin_enat_def)
done
end
instantiation ereal :: timestamp_total
begin
instance
apply standard
apply (auto simp: tfin_ereal_def)
done
end
class timestamp_total_strict = timestamp_total +
assumes add_mono_strict_total: "c < d â¹ a + c < a + d"
instantiation nat :: timestamp_total_strict
begin
instance
apply standard
apply (auto simp: tfin_nat_def)
done
end
instantiation real :: timestamp_total_strict
begin
instance
apply standard
apply (auto simp: tfin_real_def)
done
end
end
Theory Interval
theory Interval
imports "HOL-Library.Product_Lexorder" Timestamp
begin
section â¹Intervalsâº
typedef (overloaded) ('a :: timestamp) â = "{(i :: 'a, j :: 'a, lei :: bool, lej :: bool). 0 ⤠i â§ i ⤠j â§ i â tfin ⧠¬(j = 0 ⧠¬lej)}"
by (intro exI[of _ "(0, 0, True, True)"]) (auto intro: zero_tfin)
setup_lifting type_definition_â
instantiation â :: (timestamp) equal begin
lift_definition equal_â :: "'a â â 'a â â bool" is "(=)" .
instance by standard (transfer, auto)
end
lift_definition left :: "'a :: timestamp â â 'a" is "fst" .
lift_definition right :: "'a :: timestamp â â 'a" is "fst â snd" .
lift_definition memL :: "'a :: timestamp â 'a â 'a â â bool" is
"λt t' (a, b, lei, lej). if lei then t + a ⤠t' else t + a < t'" .
lift_definition memR :: "'a :: timestamp â 'a â 'a â â bool" is
"λt t' (a, b, lei, lej). if lej then t' ⤠t + b else t' < t + b" .
definition mem :: "'a :: timestamp â 'a â 'a â â bool" where
"mem t t' I â· memL t t' I â§ memR t t' I"
lemma memL_mono: "memL t t' I ⹠t'' ⤠t ⹠memL t'' t' I"
by transfer (auto simp: add.commute order_le_less_subst2 order_subst2 add_mono split: if_splits)
lemma memL_mono': "memL t t' I ⹠t' ⤠t'' ⹠memL t t'' I"
by transfer (auto split: if_splits)
lemma memR_mono: "memR t t' I ⹠t ⤠t'' ⹠memR t'' t' I"
apply transfer
apply (simp split: prod.splits)
apply (meson add_mono_comm dual_order.trans order_less_le_trans)
done
lemma memR_mono': "memR t t' I ⹠t'' ⤠t' ⹠memR t t'' I"
by transfer (auto split: if_splits)
lemma memR_dest: "memR t t' I ⹠t' ⤠t + right I"
by transfer (auto split: if_splits)
lemma memR_tfin_refl:
assumes fin: "t â tfin"
shows "memR t t I"
by (transfer fixing: t) (force split: if_splits intro: order_trans[OF _ add_mono, where ?x=t and ?a1=t and ?c1=0] add_pos[OF fin])
lemma right_I_add_mono:
fixes x :: "'a :: timestamp"
shows "x ⤠x + right I"
by transfer (auto split: if_splits intro: order_trans[OF _ add_mono, of _ _ 0])
lift_definition interval :: "'a :: timestamp â 'a â bool â bool â 'a â" is
"λi j lei lej. (if 0 ⤠i â§ i ⤠j â§ i â tfin ⧠¬(j = 0 ⧠¬lej)then (i, j, lei, lej) else Code.abort (STR ''malformed interval'') (λ_. (0, 0, True, True)))"
by (auto intro: zero_tfin)
lemma "Rep_â I = (l, r, b1, b2) â¹ memL 0 0 I â· l = 0 â§ b1"
by transfer auto
lift_definition dropL :: "'a :: timestamp â â 'a â" is
"λ(l, r, b1, b2). (0, r, True, b2)"
by (auto intro: zero_tfin)
lemma memL_dropL: "t ⤠t' ⹠memL t t' (dropL I)"
by transfer auto
lemma memR_dropL: "memR t t' (dropL I) = memR t t' I"
by transfer auto
lift_definition flipL :: "'a :: timestamp â â 'a â" is
"λ(l, r, b1, b2). if ¬(l = 0 ⧠b1) then (0, l, True, ¬b1) else Code.abort (STR ''invalid flipL'') (λ_. (0, 0, True, True))"
by (auto intro: zero_tfin split: if_splits)
lemma memL_flipL: "t ⤠t' ⹠memL t t' (flipL I)"
by transfer (auto split: if_splits)
lemma memR_flipLD: "¬memL 0 0 I ⹠memR t t' (flipL I) ⹠¬memL t t' I"
by transfer (auto split: if_splits)
lemma memR_flipLI:
fixes t :: "'a :: timestamp"
shows "(âu v. (u :: 'a :: timestamp) ⤠v ⨠v ⤠u) ⹠¬memL t t' I â¹ memR t t' (flipL I)"
by transfer (force split: if_splits)
lemma "t â tfin â¹ memL 0 0 I â· memL t t I"
apply transfer
apply (simp split: prod.splits)
apply (metis add.right_neutral add_pos antisym_conv2 dual_order.eq_iff order_less_imp_not_less)
done
definition "full (I :: ('a :: timestamp_total) â) â· (ât t'. 0 ⤠t â§ t ⤠t' â§ t â tfin â§ t' â tfin â¶ mem t t' I)"
lemma "memL 0 0 I â¹ right I â tfin â¹ full I"
unfolding full_def mem_def
by transfer (fastforce split: if_splits dest: aux)
end